; <lemma>
;  <title>SSF_pilot.4</title>
;  <origin>SSF_pilot | TCTM_Ref1 | INITIALISATION/inv6/INV</origin>
(benchmark SSF_pilot_4
;  <theories>
;    <theory name="linear_arith"/>
;  </theories>
  :logic QF_LIA
;  <typenv>
;    <variable name="x" type="INTEGER"/>
;  </typenv>
  :extrafuns ((x Int))
  :extramacros (
		 (emptyset (lambda (?x 't). false))
		 (Nat1 (lambda (?i Int) . (<= 1 ?i)))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 (in (lambda (?x 't) (?p ('t boolean)) . (?p ?x)))
		 )
; <hypothesis needed="true">x : NATURAL1</hypothesis>
  :assumption (in x Nat1)
; <goal> 0 <= x - 1</goal>
  :formula
  (not
      (<= 0 (- x 1))
    )
)
;</lemma>
